Skip to content

Least squares regression through the origin#375

Open
itsalissonsilva wants to merge 1 commit intoleanprover:mainfrom
itsalissonsilva:feat-least-squares-origin
Open

Least squares regression through the origin#375
itsalissonsilva wants to merge 1 commit intoleanprover:mainfrom
itsalissonsilva:feat-least-squares-origin

Conversation

@itsalissonsilva
Copy link

This PR adds ordinary least squares regression through the origin. It defines Sxx = ∑ xᵢ², Sxy = ∑ xᵢ yᵢ, the estimator aStar = Sxy / Sxx, and the squared loss:

loss(a) = ∑ (a * xᵢ - yᵢ)²,

and proves that aStar minimizes loss(a) assuming Sxx ≠ 0. Tests are included under CslibTests (if applicable).
Local checks: lake build, lake test.

@chenson2018
Copy link
Collaborator

Hi, thanks for your interest in contributing! However, I think this is likely more in scope for Mathlib. I would ask in the Zulip, as my assumption is that they would want a more general formulation.

@itsalissonsilva
Copy link
Author

Hey Chris, I was thinking purely in the ML aspect of it which seemed like something that would fit in CSLib. Since I plan to formalize other algorithms as well, would decision-tree classifiers or k-NN also fit in mathlib or would it fit in cslib? Sorry for the confusion.

@Shreyas4991
Copy link
Contributor

Shreyas4991 commented Feb 27, 2026

Quick comment:
Your CI checks are failing for two reasons:

  1. Your title should read something more like "feat: least squares regression through the origin"
  2. You need to run lake exe mk_all --module to ensure proper imports in Cslib.lean

Also @itsalissonsilva : numerical algorithms are traditionally a CS subject that mathematics departments might not teach. So I can't say with 100% certainty that least squares regression is outside the scope of "undergrad CS curricula", especially since they also show up in ML courses which are standard these days. But they are clearly in scope for SciLean which is a repository for algorithms of scientific computing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants